00010	VAR:x,y,z,u,s;
00020	INF_PRED:=;PRE_PRED:clear,on;
00030	PRE_OP: puton,A,B,C,T,S0,R;
00040	
00070	EQUALITY: =;
00100	clear(x,s)∧clear(y,s)⊃on(x,y,R(puton(x,y),s));
00200	clear(x,s)⊃on(x,T,R(puton(x,T),s));
00450	on(x,y,s)∧ ¬z=y ⊃clear(y,R(puton(x,z),s));
00500	
00600	clear(x,s)∧¬x=y ⊃ clear(x,R(puton(z,y),s));
00700	on(x,y,s)∧¬z=x ⊃ on(x,y,R(puton(z,u),s));
00800	clear(C,S0); clear(B,S0); 
00900	on(A,T,S0); on(B,T,S0); on(C,A,S0);
00950	¬A=B; ¬B=C; ¬C=A; ¬A=T;¬B=T; ¬C=T;
01000	THM:∃s(on(A,B,s)∧on(B,C,s));;